Termination proof of /tmp/tmpYFRFtr/OvConsOS

Termination of the following Term Rewriting System could not be shown:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
U21: {1}
nil: empty set
U31: {1}
take: {1, 2}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
U21: {1}
nil: empty set
U31: {1}
take: {1, 2}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take, LENGTH, U21¹, TAKE} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, U11¹, AND, U31¹} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, ISNAT, ISNATILIST, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U11¹(tt, L) → LENGTH(L)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(V) → ISNATLIST(V)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATLIST(take(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
LENGTH(cons(N, L)) → AND(isNatList(L), isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(L)
TAKE(0, IL) → U21¹(isNatIList(IL))
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(IL), and(isNat(M), isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)

The collapsing dependency pairs are DP_c:

U11¹(tt, L) → L
U31¹(tt, IL, M, N) → N
AND(tt, X) → X

The hidden terms of R are:

zeros
take(M, IL)
isNatIList(V2)
isNatList(V2)

Every hiding context is built from:

take on positions {1, 2}
and on positions {1}

Hence, the new unhiding pairs DP_u are :

U11¹(tt, L) → U(L)
U31¹(tt, IL, M, N) → U(N)
AND(tt, X) → U(X)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(and(x_0, x_1)) → U(x_0)
U(zeros) → ZEROS
U(take(M, IL)) → TAKE(M, IL)
U(isNatIList(V2)) → ISNATILIST(V2)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 5 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take, TAKE} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND, U31¹} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, U, ISNATILIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, X) → U(X)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(and(x_0, x_1)) → U(x_0)
U(take(M, IL)) → TAKE(M, IL)
TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATLIST(take(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U31¹(tt, IL, M, N) → U(N)
U(isNatIList(V2)) → ISNATILIST(V2)
U(isNatList(V2)) → ISNATLIST(V2)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(IL), and(isNat(M), isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = 0
POL(ISNATILIST(x₁)) = 0
POL(ISNATLIST(x₁)) = 0
POL(TAKE(x₁, x₂)) = 2·x₂
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = 2·x₁
POL(U21(x₁)) = 1 + 2·x₁
POL(U31(x₁, x₂, x₃, x₄)) = 2 + x₃ + 2·x₄
POL(U31¹(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(and(x₁, x₂)) = 2·x₁ + x₂
POL(cons(x₁, x₂)) = 2 + x₁
POL(isNat(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(length(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = 2·x₁
POL(take(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(tt) = 0
POL(zeros) = 2

the following usable rules

isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U21(tt) → nil
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
zeros → cons(0, zeros)
U31(tt, IL, M, N) → cons(N, take(M, IL))

could all be oriented weakly.
Furthermore, the pairs

U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U31¹(tt, IL, M, N) → U(N)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(IL), and(isNat(M), isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)

could be oriented strictly and thus removed.
The pairs

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATLIST(take(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatIList(V2)) → ISNATILIST(V2)
U(isNatList(V2)) → ISNATLIST(V2)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take, TAKE} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, U, ISNATILIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATLIST(take(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatIList(V2)) → ISNATILIST(V2)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, U, ISNATILIST, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATLIST(take(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = 2·x₁ + 2·x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 2·x₁
POL(ISNATLIST(x₁)) = 2·x₁
POL(U(x₁)) = 2·x₁
POL(U11(x₁, x₂)) = 2·x₂
POL(U21(x₁)) = 2 + x₁
POL(U31(x₁, x₂, x₃, x₄)) = 2 + x₂ + x₃ + x₄
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 2·x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 2 + x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATLIST(take(V1, V2)) → ISNAT(V1)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatList(V2)) → ISNATLIST(V2)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 2 + 2·x₁
POL(ISNATLIST(x₁)) = 2·x₁
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = 2·x₂
POL(U21(x₁)) = 1
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + 2·x₃ + 2·x₄
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = 2 + 2·x₁
POL(isNatList(x₁)) = 2·x₁
POL(length(x₁)) = 2·x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

ISNATILIST(V) → ISNATLIST(V)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = x₁
POL(ISNATLIST(x₁)) = x₁
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = 1 + x₂
POL(U21(x₁)) = x₁
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 1 + x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
zeros → cons(0, zeros)

could all be oriented weakly.
Furthermore, the pairs

ISNAT(length(V1)) → ISNATLIST(V1)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatList(V2)) → ISNATLIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                      ↳ QCSDPSubtermProof

                                    ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

ISNAT(s(V1)) → ISNAT(V1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ISNAT(x1) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                      ↳ QCSDPSubtermProof

                                        ↳ QCSDP

                                          ↳ PIsEmptyProof

                                    ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, U, ISNATILIST, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, X) → U(X)
U(isNatList(V2)) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the Context-Sensitive Narrowing Processor
the pair ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
was transformed to the following new pairs:

ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
ISNATILIST(cons(length(x0), y1)) → AND(isNatList(x0), isNatIList(y1))
ISNATILIST(cons(s(x0), y1)) → AND(isNat(x0), isNatIList(y1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

                                        ↳ QCSDP

                                          ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, U, ISNATILIST, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
ISNATILIST(cons(s(x0), y1)) → AND(isNat(x0), isNatIList(y1))
ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
U(isNatList(V2)) → ISNATLIST(V2)
AND(tt, X) → U(X)
ISNATILIST(cons(length(x0), y1)) → AND(isNatList(x0), isNatIList(y1))
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = 2·x₂
POL(ISNATILIST(x₁)) = 2·x₁
POL(ISNATLIST(x₁)) = 2·x₁
POL(U(x₁)) = 2·x₁
POL(U11(x₁, x₂)) = 2 + x₂
POL(U21(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₃ + 2·x₄
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 2 + x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U21(tt) → nil
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
zeros → cons(0, zeros)
U31(tt, IL, M, N) → cons(N, take(M, IL))

could all be oriented weakly.
Furthermore, the pairs

ISNATILIST(cons(length(x0), y1)) → AND(isNatList(x0), isNatIList(y1))

could be oriented strictly and thus removed.
The pairs

U(and(x_0, x_1)) → U(x_0)
ISNATILIST(cons(s(x0), y1)) → AND(isNat(x0), isNatIList(y1))
ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
U(isNatList(V2)) → ISNATLIST(V2)
AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

                                        ↳ QCSDP

                                          ↳ QCSDPReductionPairProof

                                            ↳ QCSDP

                                              ↳ QCSDPNarrowingProcessor

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, U, ISNATILIST, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
ISNATILIST(cons(s(x0), y1)) → AND(isNat(x0), isNatIList(y1))
ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
U(isNatList(V2)) → ISNATLIST(V2)
AND(tt, X) → U(X)
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the Context-Sensitive Narrowing Processor
the pair ISNATILIST(cons(s(x0), y1)) → AND(isNat(x0), isNatIList(y1))
was transformed to the following new pairs:

ISNATILIST(cons(s(0), y1)) → AND(tt, isNatIList(y1))
ISNATILIST(cons(s(length(x0)), y1)) → AND(isNatList(x0), isNatIList(y1))
ISNATILIST(cons(s(s(x0)), y1)) → AND(isNat(x0), isNatIList(y1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

                                        ↳ QCSDP

                                          ↳ QCSDPReductionPairProof

                                            ↳ QCSDP

                                              ↳ QCSDPNarrowingProcessor

                                                ↳ QCSDP

                                                  ↳ QCSDPReductionPairProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, U, ISNATILIST, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
ISNATILIST(cons(s(length(x0)), y1)) → AND(isNatList(x0), isNatIList(y1))
U(isNatList(V2)) → ISNATLIST(V2)
ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
AND(tt, X) → U(X)
ISNATILIST(cons(s(s(x0)), y1)) → AND(isNat(x0), isNatIList(y1))
ISNATILIST(cons(s(0), y1)) → AND(tt, isNatIList(y1))
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = 2·x₂
POL(ISNATILIST(x₁)) = 2·x₁
POL(ISNATLIST(x₁)) = 2·x₁
POL(U(x₁)) = 2·x₁
POL(U11(x₁, x₂)) = 2 + 2·x₂
POL(U21(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + 2·x₃ + 2·x₄
POL(and(x₁, x₂)) = 2·x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 2·x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
U11(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U21(tt) → nil
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
zeros → cons(0, zeros)
U31(tt, IL, M, N) → cons(N, take(M, IL))

could all be oriented weakly.
Furthermore, the pairs

ISNATILIST(cons(s(length(x0)), y1)) → AND(isNatList(x0), isNatIList(y1))

could be oriented strictly and thus removed.
The pairs

U(and(x_0, x_1)) → U(x_0)
U(isNatList(V2)) → ISNATLIST(V2)
ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
AND(tt, X) → U(X)
ISNATILIST(cons(s(s(x0)), y1)) → AND(isNat(x0), isNatIList(y1))
ISNATILIST(cons(s(0), y1)) → AND(tt, isNatIList(y1))
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDPReductionPairProof

                              ↳ QCSDP

                                ↳ QCSDependencyGraphProof

                                  ↳ AND

                                    ↳ QCSDP

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

                                        ↳ QCSDP

                                          ↳ QCSDPReductionPairProof

                                            ↳ QCSDP

                                              ↳ QCSDPNarrowingProcessor

                                                ↳ QCSDP

                                                  ↳ QCSDPReductionPairProof

                                                    ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, U, ISNATLIST, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatList(V2)) → ISNATLIST(V2)
ISNATILIST(cons(0, y1)) → AND(tt, isNatIList(y1))
AND(tt, X) → U(X)
ISNATILIST(cons(s(s(x0)), y1)) → AND(isNat(x0), isNatIList(y1))
ISNATILIST(cons(s(0), y1)) → AND(tt, isNatIList(y1))
U(isNatIList(V2)) → ISNATILIST(V2)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, U21, take, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, U31, and, U11¹} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
U11¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → U31ACTIVE(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(take(x1, x2)) → MARK(x2)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(U11(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(cons(x1, x2)) → MARK(x1)
MARK(zeros) → ZEROSACTIVE
U11ACTIVE(tt, L) → MARK(L)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, X) → MARK(X)
MARK(U31(x1, x2, x3, x4)) → U31ACTIVE(mark(x1), x2, x3, x4)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatIListActive(IL), and(isNat(M), isNat(N)))
TAKEACTIVE(0, IL) → U21ACTIVE(isNatIListActive(IL))
MARK(and(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(take(x1, x2)) → MARK(x1)
MARK(U31(x1, x2, x3, x4)) → MARK(x1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)
ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1)) → MARK(x1)
MARK(U21(x1)) → U21ACTIVE(mark(x1))
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNat(N))
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
U31ACTIVE(tt, IL, M, N) → MARK(N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → U31ACTIVE(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(take(x1, x2)) → MARK(x2)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(U11(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(cons(x1, x2)) → MARK(x1)
MARK(zeros) → ZEROSACTIVE
U11ACTIVE(tt, L) → MARK(L)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, X) → MARK(X)
MARK(U31(x1, x2, x3, x4)) → U31ACTIVE(mark(x1), x2, x3, x4)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatIListActive(IL), and(isNat(M), isNat(N)))
TAKEACTIVE(0, IL) → U21ACTIVE(isNatIListActive(IL))
MARK(and(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(take(x1, x2)) → MARK(x1)
MARK(U31(x1, x2, x3, x4)) → MARK(x1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)
ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1)) → MARK(x1)
MARK(U21(x1)) → U21ACTIVE(mark(x1))
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNat(N))
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
U31ACTIVE(tt, IL, M, N) → MARK(N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(take(x1, x2)) → MARK(x2)
TAKEACTIVE(s(M), cons(N, IL)) → U31ACTIVE(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(U11(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(cons(x1, x2)) → MARK(x1)
U11ACTIVE(tt, L) → MARK(L)
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, X) → MARK(X)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
MARK(U31(x1, x2, x3, x4)) → U31ACTIVE(mark(x1), x2, x3, x4)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatIListActive(IL), and(isNat(M), isNat(N)))
MARK(and(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(take(x1, x2)) → MARK(x1)
MARK(U31(x1, x2, x3, x4)) → MARK(x1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)
ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNat(N))
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
U31ACTIVE(tt, IL, M, N) → MARK(N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(take(x1, x2)) → MARK(x2)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(U11(x1, x2)) → MARK(x1)
MARK(length(x1)) → MARK(x1)
MARK(U31(x1, x2, x3, x4)) → U31ACTIVE(mark(x1), x2, x3, x4)
MARK(take(x1, x2)) → MARK(x1)
MARK(U31(x1, x2, x3, x4)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → U31ACTIVE(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(cons(x1, x2)) → MARK(x1)
U11ACTIVE(tt, L) → MARK(L)
ANDACTIVE(tt, X) → MARK(X)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatIListActive(IL), and(isNat(M), isNat(N)))
MARK(and(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)
ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNat(N))
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
U31ACTIVE(tt, IL, M, N) → MARK(N)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = 1 + x₂
POL(ISNATACTIVE(x₁)) = 1
POL(ISNATILISTACTIVE(x₁)) = 1
POL(ISNATLISTACTIVE(x₁)) = 1
POL(LENGTHACTIVE(x₁)) = 1 + x₁
POL(MARK(x₁)) = 1 + x₁
POL(TAKEACTIVE(x₁, x₂)) = 1 + x₂
POL(U11(x₁, x₂)) = 1 + x₁ + x₂
POL(U11ACTIVE(x₁, x₂)) = 1 + x₂
POL(U11Active(x₁, x₂)) = 1 + x₁ + x₂
POL(U21(x₁)) = 1 + x₁
POL(U21Active(x₁)) = 1 + x₁
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(U31ACTIVE(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U31Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatActive(length(V1)) → isNatListActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
mark(isNatList(x1)) → isNatListActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
mark(isNat(x1)) → isNatActive(x1)
andActive(tt, X) → mark(X)
isNatActive(s(V1)) → isNatActive(V1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatIListActive(V) → isNatListActive(V)
lengthActive(x1) → length(x1)
andActive(x1, x2) → and(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
isNatActive(x1) → isNat(x1)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
mark(zeros) → zerosActive
zerosActive → cons(0, zeros)
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
isNatActive(0) → tt
U21Active(tt) → nil
U11Active(tt, L) → s(lengthActive(mark(L)))
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
takeActive(0, IL) → U21Active(isNatIListActive(IL))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → U31ACTIVE(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(cons(x1, x2)) → MARK(x1)
U11ACTIVE(tt, L) → MARK(L)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ANDACTIVE(tt, X) → MARK(X)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatIListActive(IL), and(isNat(M), isNat(N)))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)
ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNat(N))
U31ACTIVE(tt, IL, M, N) → MARK(N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 8 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                      ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
MARK(cons(x1, x2)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ANDACTIVE(tt, X) → MARK(X)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(and(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATACTIVE(length(V1)) → ISNATLISTACTIVE(V1)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(V1)) → ISNATACTIVE(V1)
MARK(cons(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ISNATLISTACTIVE(take(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(and(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATLISTACTIVE(take(V1, V2)) → ISNATACTIVE(V1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatIList(V2))
MARK(isNat(x1)) → ISNATACTIVE(x1)

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))
ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ANDACTIVE(tt, X) → MARK(X)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = 1 + x₂
POL(ISNATACTIVE(x₁)) = 1 + x₁
POL(ISNATILISTACTIVE(x₁)) = 1 + x₁
POL(ISNATLISTACTIVE(x₁)) = 1 + x₁
POL(MARK(x₁)) = 1 + x₁
POL(U11(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = 0
POL(U21(x₁)) = 0
POL(U21Active(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = 0
POL(U31Active(x₁, x₂, x₃, x₄)) = 0
POL(and(x₁, x₂)) = 1 + x₁ + x₂
POL(andActive(x₁, x₂)) = 0
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(isNat(x₁)) = 1 + x₁
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 1 + x₁
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = 1 + x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 0
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented: none

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                      ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ANDACTIVE(tt, X) → MARK(X)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatActive(V1), isNatList(V2))

The remaining pairs can at least be oriented weakly.

ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ANDACTIVE(tt, X) → MARK(X)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = 1 + x₂
POL(ISNATILISTACTIVE(x₁)) = 1 + x₁
POL(ISNATLISTACTIVE(x₁)) = 1 + x₁
POL(MARK(x₁)) = 1 + x₁
POL(U11(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = 0
POL(U21(x₁)) = 0
POL(U21Active(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = 0
POL(U31Active(x₁, x₂, x₃, x₄)) = 0
POL(and(x₁, x₂)) = 0
POL(andActive(x₁, x₂)) = 0
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = 0
POL(take(x₁, x₂)) = 0
POL(takeActive(x₁, x₂)) = 0
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented: none

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ DependencyGraphProof

                      ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(V) → ISNATLISTACTIVE(V)
ANDACTIVE(tt, X) → MARK(X)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U11ACTIVE(tt, L) → LENGTHACTIVE(mark(L)) at position [0] we obtained the following new rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U11ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, 0) → LENGTHACTIVE(0)
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U11ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U11ACTIVE(tt, nil) → LENGTHACTIVE(nil)
U11ACTIVE(tt, U21(x0)) → LENGTHACTIVE(U21Active(mark(x0)))
U11ACTIVE(tt, tt) → LENGTHACTIVE(tt)
U11ACTIVE(tt, s(x0)) → LENGTHACTIVE(s(mark(x0)))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U11ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, 0) → LENGTHACTIVE(0)
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U11ACTIVE(tt, U21(x0)) → LENGTHACTIVE(U21Active(mark(x0)))
U11ACTIVE(tt, nil) → LENGTHACTIVE(nil)
U11ACTIVE(tt, tt) → LENGTHACTIVE(tt)
U11ACTIVE(tt, s(x0)) → LENGTHACTIVE(s(mark(x0)))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U11ACTIVE(tt, U21(x0)) → LENGTHACTIVE(U21Active(mark(x0)))
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U11ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive) at position [0] we obtained the following new rules:

U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(zeros)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U11ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U11ACTIVE(tt, U21(x0)) → LENGTHACTIVE(U21Active(mark(x0)))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(zeros)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U11ACTIVE(tt, U21(x0)) → LENGTHACTIVE(U21Active(mark(x0)))
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U11ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U11ACTIVE(tt, U21(x0)) → LENGTHACTIVE(U21Active(mark(x0)))

The remaining pairs can at least be oriented weakly.

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11ACTIVE(x₁, x₂)) = x₁
POL(U11Active(x₁, x₂)) = 0
POL(U21(x₁)) = 0
POL(U21Active(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = 0
POL(U31Active(x₁, x₂, x₃, x₄)) = 1
POL(and(x₁, x₂)) = 0
POL(andActive(x₁, x₂)) = x₁
POL(cons(x₁, x₂)) = 1
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 1
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 1
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 0
POL(takeActive(x₁, x₂)) = 1
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
isNatListActive(x1) → isNatList(x1)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
isNatActive(length(V1)) → isNatListActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
mark(isNatList(x1)) → isNatListActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
mark(isNat(x1)) → isNatActive(x1)
andActive(tt, X) → mark(X)
isNatActive(s(V1)) → isNatActive(V1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatIListActive(V) → isNatListActive(V)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
andActive(x1, x2) → and(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
isNatActive(x1) → isNat(x1)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(zeros) → zerosActive
mark(nil) → nil
zerosActive → cons(0, zeros)
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
isNatActive(0) → tt
U21Active(tt) → nil
U11Active(tt, L) → s(lengthActive(mark(L)))
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
takeActive(0, IL) → U21Active(isNatIListActive(IL))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U11ACTIVE(tt, U31(x0, x1, x2, x3)) → LENGTHACTIVE(U31Active(mark(x0), x1, x2, x3))
U11ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))

The remaining pairs can at least be oriented weakly.

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11ACTIVE(x₁, x₂)) = x₁ + x₂
POL(U11Active(x₁, x₂)) = 1
POL(U21(x₁)) = 0
POL(U21Active(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂
POL(U31Active(x₁, x₂, x₃, x₄)) = 1 + x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 1 + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 1
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 1
POL(length(x₁)) = 1
POL(lengthActive(x₁)) = 1
POL(mark(x₁)) = 1 + x₁
POL(nil) = 0
POL(s(x₁)) = 0
POL(take(x₁, x₂)) = x₂
POL(takeActive(x₁, x₂)) = x₂
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
isNatListActive(x1) → isNatList(x1)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
isNatActive(length(V1)) → isNatListActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
mark(isNatList(x1)) → isNatListActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
mark(isNat(x1)) → isNatActive(x1)
andActive(tt, X) → mark(X)
isNatActive(s(V1)) → isNatActive(V1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatIListActive(V) → isNatListActive(V)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
andActive(x1, x2) → and(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
isNatActive(x1) → isNat(x1)
mark(U21(x1)) → U21Active(mark(x1))
isNatIListActive(x1) → isNatIList(x1)
U21Active(x1) → U21(x1)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(zeros) → zerosActive
mark(nil) → nil
zerosActive → cons(0, zeros)
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
isNatActive(0) → tt
U21Active(tt) → nil
U11Active(tt, L) → s(lengthActive(mark(L)))
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
takeActive(0, IL) → U21Active(isNatIListActive(IL))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U11ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))

The remaining pairs can at least be oriented weakly.

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11ACTIVE(x₁, x₂)) = x₁ + x₂
POL(U11Active(x₁, x₂)) = 0
POL(U21(x₁)) = 0
POL(U21Active(x₁)) = 0
POL(U31(x₁, x₂, x₃, x₄)) = x₂
POL(U31Active(x₁, x₂, x₃, x₄)) = 1 + x₂
POL(and(x₁, x₂)) = 1 + x₂
POL(andActive(x₁, x₂)) = 1 + x₂
POL(cons(x₁, x₂)) = 1 + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 1
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 1
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1 + x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₂
POL(takeActive(x₁, x₂)) = x₂
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
isNatListActive(x1) → isNatList(x1)
isNatActive(length(V1)) → isNatListActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
mark(isNatList(x1)) → isNatListActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
mark(isNat(x1)) → isNatActive(x1)
andActive(tt, X) → mark(X)
isNatActive(s(V1)) → isNatActive(V1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatIListActive(V) → isNatListActive(V)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
andActive(x1, x2) → and(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(x1) → isNat(x1)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
isNatIListActive(x1) → isNatIList(x1)
U21Active(x1) → U21(x1)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(zeros) → zerosActive
mark(nil) → nil
zerosActive → cons(0, zeros)
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
isNatActive(0) → tt
U21Active(tt) → nil
U11Active(tt, L) → s(lengthActive(mark(L)))
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
takeActive(0, IL) → U21Active(isNatIListActive(IL))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U11ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U11ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U11ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))

The remaining pairs can at least be oriented weakly.

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11ACTIVE(x₁, x₂)) = 1
POL(U11Active(x₁, x₂)) = 0
POL(U21(x₁)) = 1
POL(U21Active(x₁)) = 1
POL(U31(x₁, x₂, x₃, x₄)) = 1
POL(U31Active(x₁, x₂, x₃, x₄)) = 1
POL(and(x₁, x₂)) = x₂
POL(andActive(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = 1
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = x₁
POL(nil) = 1
POL(s(x₁)) = 0
POL(take(x₁, x₂)) = 1
POL(takeActive(x₁, x₂)) = 1
POL(tt) = 0
POL(zeros) = 1
POL(zerosActive) = 1

The following usable rules [17] were oriented:

takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatActive(length(V1)) → isNatListActive(V1)
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
mark(isNatList(x1)) → isNatListActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
mark(isNat(x1)) → isNatActive(x1)
andActive(tt, X) → mark(X)
isNatActive(s(V1)) → isNatActive(V1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatIListActive(V) → isNatListActive(V)
lengthActive(x1) → length(x1)
andActive(x1, x2) → and(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(x1) → isNat(x1)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
isNatIListActive(x1) → isNatIList(x1)
U21Active(x1) → U21(x1)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(zeros) → zerosActive
mark(nil) → nil
zerosActive → cons(0, zeros)
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
isNatActive(0) → tt
U21Active(tt) → nil
U11Active(tt, L) → s(lengthActive(mark(L)))
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
takeActive(0, IL) → U21Active(isNatIListActive(IL))
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

                                                      ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U11ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(andActive(isNatListActive(L), isNat(N)), L)
U11ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U21(x1)) → U21Active(mark(x1))
U21Active(x1) → U21(x1)
mark(U31(x1, x2, x3, x4)) → U31Active(mark(x1), x2, x3, x4)
U31Active(x1, x2, x3, x4) → U31(x1, x2, x3, x4)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt) → nil
U31Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → isNatListActive(V1)
isNatActive(s(V1)) → isNatActive(V1)
isNatIListActive(V) → isNatListActive(V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → andActive(isNatActive(V1), isNatList(V2))
isNatListActive(take(V1, V2)) → andActive(isNatActive(V1), isNatIList(V2))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(andActive(isNatListActive(L), isNat(N)), L)
takeActive(0, IL) → U21Active(isNatIListActive(IL))
takeActive(s(M), cons(N, IL)) → U31Active(andActive(isNatIListActive(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Trivial transformation to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(V1, V2)) → ISNAT(V1)
ZEROS → ZEROS
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)
LENGTH(cons(N, L)) → ISNATLIST(L)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
TAKE(s(M), cons(N, IL)) → AND(isNatIList(IL), and(isNat(M), isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNAT(M)
TAKE(s(M), cons(N, IL)) → AND(isNat(M), isNat(N))
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
ISNAT(length(V1)) → ISNATLIST(V1)
LENGTH(cons(N, L)) → ISNAT(N)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
ISNATILIST(cons(V1, V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(take(V1, V2)) → ISNATILIST(V2)
TAKE(0, IL) → U21¹(isNatIList(IL))
LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
ISNATLIST(cons(V1, V2)) → ISNATLIST(V2)
LENGTH(cons(N, L)) → AND(isNatList(L), isNat(N))
TAKE(0, IL) → ISNATILIST(IL)
ISNAT(s(V1)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U11¹(tt, L) → LENGTH(L)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U31¹(tt, IL, M, N) → TAKE(M, IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(V1, V2)) → ISNAT(V1)
ZEROS → ZEROS
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)
LENGTH(cons(N, L)) → ISNATLIST(L)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
TAKE(s(M), cons(N, IL)) → AND(isNatIList(IL), and(isNat(M), isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNAT(M)
TAKE(s(M), cons(N, IL)) → AND(isNat(M), isNat(N))
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
ISNAT(length(V1)) → ISNATLIST(V1)
LENGTH(cons(N, L)) → ISNAT(N)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
ISNATILIST(cons(V1, V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(take(V1, V2)) → ISNATILIST(V2)
TAKE(0, IL) → U21¹(isNatIList(IL))
LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
ISNATLIST(cons(V1, V2)) → ISNATLIST(V2)
LENGTH(cons(N, L)) → AND(isNatList(L), isNat(N))
TAKE(0, IL) → ISNATILIST(IL)
ISNAT(s(V1)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
U11¹(tt, L) → LENGTH(L)
ISNATLIST(take(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U31¹(tt, IL, M, N) → TAKE(M, IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 13 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → ISNATLIST(V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATILIST(cons(V1, V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(take(V1, V2)) → ISNATILIST(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → ISNATLIST(V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → ISNATILIST(V2)
ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(take(V1, V2)) → ISNATILIST(V2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ISNAT(length(V1)) → ISNATLIST(V1)
The graph contains the following edges 1 > 1
ISNAT(s(V1)) → ISNAT(V1)
The graph contains the following edges 1 > 1
ISNATLIST(cons(V1, V2)) → ISNATLIST(V2)
The graph contains the following edges 1 > 1
ISNATILIST(V) → ISNATLIST(V)
The graph contains the following edges 1 >= 1
ISNATLIST(take(V1, V2)) → ISNATILIST(V2)
The graph contains the following edges 1 > 1
ISNATILIST(cons(V1, V2)) → ISNATILIST(V2)
The graph contains the following edges 1 > 1
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
The graph contains the following edges 1 > 1
ISNATLIST(take(V1, V2)) → ISNAT(V1)
The graph contains the following edges 1 > 1
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
The graph contains the following edges 1 > 1

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
U31¹(tt, IL, M, N) → TAKE(M, IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U31¹(tt, IL, M, N) → TAKE(M, IL)
The graph contains the following edges 3 >= 1, 2 >= 2
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)
The graph contains the following edges 2 > 2, 1 > 3, 2 > 4

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
U11¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

From the DPs we obtained the following set of size-change graphs:

U11¹(tt, L) → LENGTH(L)
The graph contains the following edges 2 >= 1
LENGTH(cons(N, L)) → U11¹(and(isNatList(L), isNat(N)), L)
The graph contains the following edges 1 > 2

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
U21(tt) → nil
U31(tt, IL, M, N) → cons(N, take(M, IL))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNatList(take(V1, V2)) → and(isNat(V1), isNatIList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.